Топология на 10 LOC. Определение

Definition subset (A : Type) (u v : A -> Prop) := (forall x : A, u x -> v x).
Definition union (A : Type) (B : (A -> Prop) -> Prop) := fun x : A => exists U,
B U /\ U x.
Definition inter (A : Type) (u v : A -> Prop) := fun x : A => u x /\ v x.
Definition empty (A: Type) := fun x : A => False.
Definition full (A: Type) := fun x : A => True.

Structure topology (A : Type) := {
          open :> (A -> Prop) -> Prop;
          empty_open: open (empty _);
          full_open: open (full _);
          inter_open: forall u, open u -> forall v, open v -> open (inter A uv) ;
          union_open: forall s, (subset _ s open) -> open (union A s) }.